(cgol) $

% McCarthy's monkey-and-bananas problem, DL version.  %

start $ remob "ON" $

% At present (2/2/78) the checker cannot handle uninterpreted programs having
parameters, so these peculiar definitions of move, climb, reach are given. Igy|them.  %

move(a,b,c):  m;a;b;c $
climb(a,b): cl;a;b $
reach(p,x): r;p;x $

% The main theorem %

show <move(monkey, box, under←bananas);
      climb(monkey, box);
      reach(monkey, bananas)> has(monkey, bananas)

using	<move(monkey,box,u)>t,
	[move(p,v,u)]at(v,u),
	<climb(monkey,box)>t,
	at(v,u) ⊃ [climb(p,v)](at(v,u) ∧ on(p,v)),
	(at(box, under←bananas) ∧ on(monkey, box)) ⊃ <reach(monkey, bananas)>t,
	[reach(p,x)]has(p,x)

binding {u,2} -> monkey, {p,3} -> monkey, {v,3} -> box, {u,3} -> under←bananas,
	{v,5} -> box, {u,5} -> under←bananas, {p,5} -> monkey,
	{p,7} -> monkey, {x,7} -> bananas $

=exit$